the_es:ES, e:E, l:IdLnk, m:Msg, i:, e1:E.
(i < ||sends(l;e)||)
 (m = sends(l;e)[i])
 (isrcv(e1))
 (lnk(e1) = l)
 (tag(e1) = mtag(m)  Id)
 (msgtype(m) = valtype(e1)  Type) 

latex

Definitions	t  T, {T}, P  Q, x:A. B(x), SQType(T), IdLnk, s = t, , ||as||, s ~ t, False, A, A  B, , {x:A| B(x)} , , x:A  B(x), lnk(e), mlnk(m), <a, b>, es-M(es), f(a), Id, Type, x:AB(x), mtag(m), rcvtype(e), msgtype(m), b, b, , isrcv(e), P & Q, P  Q, Unit, left + right, valtype(e), (Msg on l), ES, E, Msg, sends(l;e), a < b, #$n, Void, type List, S  T, l[i], tag(e), haslink(l;m), Msg(M)
Lemmas	Id wf, es-tag wf, es-mtag wf, es-lnk wf, select wf, length wf1, es-Msgl wf, es-sends wf, nat wf, es-Msg wf, es-E wf, event system wf, es-mval wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, es-isrcv wf, bool wf, bnot wf, not wf, assert wf, es-M wf, IdLnk wf, IdLnk sq